A:MsgA, x:Id, k:Knd.
Feasible(A)  <k,x>  dom(1of(2of(2of(2of(2of(A)))))) = true    A.aframe(k affects x) 

latex

Definitions

x:A. B(x), P & Q, b, t  T, Id, x:AB(x), Knd, x:AB(x), S  T, P  Q, IdLnk, P  Q, Void, Type, x.A(x), x. t(x), 2of(t), IdDeq, f(x)?z, Top, 1of(t), KindDeq, State(ds), a:A fp B(a), true, product-deq(A;B;a;b), x  dom(f), , s = t, Prop, type List, z != f(x)  P(a;z), xdom(f). v=f(x)   P(x;v), M.da(a), M.state, M.rframe(A.sends tfL of k on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B), Valtype(da;k), MsgA, Feasible(M), <a,b>

Lemmas

msga wf, ma-feasible wf, bool wf, fpf-dom wf, product-deq wf, btrue wf, fpf-trivial-subtype-top, ma-state wf, Kind-deq wf, pi1 wf, top wf, fpf-cap wf, id-deq wf, pi2 wf, Knd wf, Id wf, eqtt to assert